COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00006 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.cb reply to Burger

	My %2samefringe%1 includes all atoms in an S-expression while
Burger's omits the qNILs at the ends of lists.  Mine corresponds to
the definition

!!a1:	%2fringe x ← qif qat x qthen <x> qelse fringe qa x * fringe qd x%1,

where * is an infix for the associative operation %2append%1.
Using the results of (Cartwright 1977), we can characterize %2gopher%1
by the sentence

!!a3:	%2∀x.(gopher x = qif qat qa x qthen x qelse
gopher[qaa x .[qda x . qd x]])%1

of first order logic.  (Conditional expressions are admitted as terms
as in (Manna 1974), and the %2a priori%1 possibility that %2gopher%1
may not be total is provided for by not assuming that %2gopher_x%1
is an S-expression and leaving it to be proved as an expression of
termination.
The total correctess of %2gopher%1 is then expressed by the formula

!!a2:	%2∀ x y.(issexp gopher[x.y] ∧ qat qa gopher[x.y] ∧
fringe gopher[x.y] = fringe[x.y])%1,

where the first conjunct says that %2gopher[x.y]%1 is an S-expression,
(i.e. that %2gopher%1 is total on non-atoms), the second says that
its %2car%1 is atomic (which actually implies totality), and the
last says that gopher doesn't change the fringe.

	({eq a2}) is readily proved by structural induction using
the predicate

!!a4:	%2P(x) ≡ ∀y.(issexp gopher[x.y] ∧ qat qa gopher[x.y] ∧
fringe gopher[x.y] = fringe[x.y])%1,

structural induction being expressed by the axiom schema

!!a4a:	%2∀x.(qat x ⊃ P(x)) ∧ ∀x.(¬qat x ∧ P(qa x) ∧ P(qd x) ⊃ P(x))
⊃ Nx.P(x)%1.

	The proof uses the first order axioms for the Lisp functions,
the associativity of the * connective, and the formula

!!a5:	%2∀x y.(fringe[x.y] = fringe x * fringe y)%1

which follows immediately from the first order formula defining %2fringe%1
once it has been proved (by structural induction) that %2fringe%1 is total.

	A formal proof in the FOL proof checker (Weyhrauch 197x) involves
yyy steps requiring the typing of zzz characters to the proof checker.

	The correctness of %2samefringe%1 itself is longer to state and
prove, because they involve simultaneous recursions and because we need two
flavors of Boolean connectives - the ordinary ones and continuous ones
that take values in a domain %AP%1_=_α{T,F,%Aw%1α}, where %Aw%1
represents the undefined element.